Variable Resolution Discretization in Optimal Control

The problem of state abstraction is of central importance in optimal control, reinforcement learning and Markov decision processes. This paper studies the case of variable resolution state abstraction for continuous time and space, deterministic dynamic control problems in which near-optimal policies are required. We begin by defining a class of variable resolution policy and value function representations based on Kuhn triangulations embedded in a kd-trie. We then consider top-down approaches to choosing which cells to split in order to generate improved policies. The core of this paper is the introduction and evaluation of a wide variety of possible splitting criteria. We begin with local approaches based on value function and policy properties that use only features of individual cells in making split choices. Later, by introducing two new non-local measures, influence and variance, we derive splitting criteria that allow one cell to efficiently take into account its impact on other cells when deciding whether to split. Influence is an efficiently-calculable measure of the extent to which changes in some state effect the value function of some other states. Variance is an efficiently-calculable measure of how risky is some state in a Markov chain: a low variance state is one in which we would be very surprised if, during any one execution, the long-term reward attained from that state differed substantially from its expected value, given by the value function.The paper proceeds by graphically demonstrating the various approaches to splitting on the familiar, non-linear, non-minimum phase, and two dimensional problem of the Car on the hill. It then evaluates the performance of a variety of splitting criteria on many benchmark problems, paying careful attention to their number-of-cells versus closeness-to-optimality tradeoff curves.     

The complexity of checking consistency of pedigree information and related problems

Consistency checking is a fundamental computational problem in genetics. Given a pedigree and information on the genotypes (of some) of the individuals in it, the aim of consistency checking is to determine whether these data are consistent with the classic Mendelian laws of inheritance. This problem arose originally from the geneticists‘ need to filter their input data from erroneous information, and is well motivated from both a biological and a sociological viewpoint. This paper shows that consistency checking is NP-complete, even with focus on a single gene and in the presence of three alleles. Several other results on the computational complexity of problems from genetics that are related to consistency checking are also offered. In particular, it is shown that checking the consistency of pedigrees over two alleles, and of pedigrees without loops, can be done in polynomial time.     

基于模型检测的领域约束规划

基于模型检测的智能规划是当今通用的智能规划研究的热点,其求解效率比较高.但是,目前基于模型检测的智能规划系统没有考虑到利用领域知识来提高描述能力和求解效率.为此,研究了增加领域约束的基于模型检测的智能规划方法,并据此建立了基于模型检测的领域约束规划系统DCIPS(domain constraints integrated planning system).它主要考虑了领域知识在规划中的应用,将领域知识表示为领域约束添加到规划系统中.根据"规划=动作+状态",DCIPS将领域约束分为3种,即对象约束、过程约束和时序约束,采用对象约束来表达状态中对象之间的关系,采用过程约束来表达动作之间的关系,采用时序约束表达动作与状态中对象之间的关系.通过在2002年智能规划大赛AIPS 2002上关于交通运输领域的3个例子的测试,实验结果表明,利用领域约束的DCIPS可以方便地增加领域知识,更加实用化,其效率也有了相应的提高.     

Polygonal space carving with geometric anti-aliasing

This paper proposes an algorithm that solves the shape recovery problem from N arbitrary images. By introducing a polygonal carving technique, the proposed algorithm can reconstruct the image-consistent polygonal shape that is patched by input images. This algorithm eliminates the invalid vertices and polygons from the initial polygonal grid space according to the color variance that represents their image consistency. The carved shape is refined by moving the outlier vertices on the boundary of each image. The final reconstructed shape faithfully accounts for the input images, and its textured appearance reflects the similar color property of the target object.     

ERC – An object-oriented refinement calculus for Eiffel

We present a refinement calculus for transforming object-oriented (OO) specifications (or contracts) of classes into executable Eiffel programs. The calculus includes the usual collection of algorithmic refinement rules for assignments, if-statements, and loops. However, the calculus also deals with some of the specific challenges of OO, namely rules for introducing feature calls and reference types (involving aliasing). The refinement process is compositional in the sense that a class specification is refined to code based only on the specifications (not the implementations) of the classes that the specification depends upon. We discuss how automated support for such a process can be developed based on existing tools. This work is done in the context of a larger project involving methods for the seamless design of OO software in the graphical design notation BON (akin to UML). The goal is to maintain model and source code integrity, i.e., the software developer can work on either the model or the code, where (ideally) changes in one view are reflected instantaneously and automatically in all views.Correspondence and offprint request to: Richard F. Paige, Department of Computer Science, University of York, Heslington, York, YO10 5DD, United Kingdom. Email: paige@cs.york.ac.ukThe authors thank the National Sciences and Engineering Research Council of Canada for their support.Received January 2000 Accepted in revised August 2003 by B.C. Pierce     

EvIA - Evidential Interval Algebra and Heuristic Backtrack-Free Algorithm

The Interval Algebra (IA) framework for temporal reasoning encodes indefinite knowledge in terms of disjunctions of relations. Many problems arising in practice can have evidences from past or from other external sources to indicate that some relations in a disjunction may be more probable than others. IA framework is inadequate to encode this information. The aim of the present study is two fold. First, to extend IA framework by associating numeric weights to the relations for capturing additional information and provide a reasoning methodology for the extended framework. Second, to apply the extended framework for developing a heuristic algorithm which finds a solution of the conventional IA network problem without backtrack. We make use of well-known evidential reasoning techniques to develop the new framework, Evidential Interval Algebra (EvIA). EvIA is an augmentation of interval algebra with evidential techniques. The constraint, constraint operators namely converse, composition and intersection, and path consistency algorithm of interval algebra are overlayed by evidential function and evidential operations to get enhanced expressiveness and efficient reasoning capability. The efficiency of the EvIA framework is demonstrated in the form of a heuristic which finds a solution of the interval algebra network without backtrack. Experimental results of the heuristic algorithm reveal that the algorithm is sound and for some specific types of the problems, the success of finding a solution is more than 90 percent. The results also show that the algorithm is efficient in terms of runtime when compared with a backtrack search algorithm.     

A case study on applying formal methods to medical devices: computer-aided resuscitation algorithm

The design and functional complexity of medical devices have increased during the past 50 years, evolving from the use of a metronome circuit for the initial cardiac pacemaker to functions that include electrocardiogram analysis, laser surgery, and intravenous delivery systems that adjust dosage based on patient feedback. As device functionality becomes more intricate, concerns arise regarding efficacy, safety, and reliability. It thus becomes imperative to adopt a standard or methodology to ensure that the possibility of any defect or malfunction in these devices is minimized. It is with these facts in view that regulatory bodies are interested in investigating mechanisms to certify safety-crictical medical devices. These organizations advocate the use of formal methods techniques to evaluate safety-critical medical systems. However, the use of formal methods is keenly debated, with most manufacturers claiming that they are arduous and time consuming.In this paper we describe our experience in analyzing the requirements documents for the computer-aided resuscitation algorithm (CARA) designed by the Resuscitative Unit of the Walter Reed Army Institute of Research (WRAIR). We present our observations from two different angles – that of a nonbeliever in formal methods and that of a practitioner of formal methods. For the former we catalog the effort required by a novice user of formal methods tools to carry out an analysis of the requirements documents. For the latter we address issues related to choice of designs, errors in discovered requirements, and the tool support available for analyzing requirements .     

Guest editors’ introduction: Advancements and extensions of verification techniques

This special section is devoted to a selection of journal versions of papers that appeared originally in the Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), which took place in Grenoble, France in April 2002 as a constituent event of the European joint conferences on Theory and Practice of Software (ETAPS). All papers are relevant to the field of systems validation. The first three papers advance and extend model-checking techniques, the fourth presents algorithms for run-time verification, and the last paper is about animation and test generation for formal system specifications.     

Model-based testing for real

Model-based testing relies on abstract behavior models for test case generation. These models are abstractions, i.e., simplifications. For deterministic reactive systems, test cases are sequences of input and expected output. To bridge the different levels of abstraction, input must be concretized before being applied to the system under test. The systems output must then be abstracted before being compared to the output of the model.The concepts are discussed along the lines of a feasibility study, an inhouse smart card case study. We describe the modeling concepts of the CASE tool AutoFocus and an approach to model-based test case generation that is based on symbolic execution with Constraint Logic Programming.Different search strategies and algorithms for test case generation are discussed. Besides validating the model itself, generated test cases were used to verify the actual hardware with respect to these traces.